\begin{tabbing}
\%\= (Auto\_aux (first\_nat 1:n) ((first\_nat 1:n),(first\_nat 1000:n)) (first\_tok :t) inil\_term)\+
\\[0ex]s\=hould have got this, but type inf failed \+
\\[0ex]on untyped lambda$\ldots\,$ \% 
\-\-\\[0ex]Reduce 0
\end{tabbing}